Nuprl Lemma : compat-append
11,40
postcript
pdf
T
:Type,
as
,
cs
,
bs
,
ds
:(
T
List). compat(
T
; append(
as
;
bs
); append(
cs
;
ds
))
compat(
T
;
as
;
cs
)
latex
Definitions
t
T
,
compat(
T
;
l1
;
l2
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
iseg(
T
;
l1
;
l2
)
,
P
Q
,
append(
as
;
bs
)
,
guard(
T
)
,
P
Q
,
P
Q
,
P
Q
Lemmas
compat-cons
,
nil
iseg
,
compat
wf
,
append
wf
,
iseg
wf
origin
T:Type, as,cs,bs,ds:(T List). compat(T; append(as; bs); append(cs; ds)) 
compat(T; as; cs) T:Type, as,cs,bs,ds:(T List). compat(T; append(as; bs); append(cs; ds)) compat(T; as; cs) 
T Qx:A. B(x)
Q
Q
Q Q